/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */
/**
 * NuGat-API named Chameleon developed by Simon De Baets to Verimag.
 *
 */
package chameleon.model.NuGatStructure.bdd;

import chameleon.gameSolver.NuGat.NuGatInterface;
import chameleon.model.NuGatStructure.NuGatStructure;
import com.sun.jna.Pointer;
import java.util.Vector;

/**
 * This class is a wrapper to the C struct dd.c. Finaly use Cudd.
 * @author simon
 */
public class DdManager extends NuGatStructure {
    
    public DdManager(Pointer ddManager, NuGatInterface nugat){
        super(ddManager,nugat);
    }
    
    /**
     * Return the bddOne
     * 
     * @return bdd_ptr
     */
    
    public Bdd bddOne(){
        return new Bdd (nugat_.bdd_one(this.ptr()),nugat_);
    }
    
    /**
     * return the bddZero
     * @return bdd_ptr
     */
    public Bdd bddZero(){
        return new Bdd (nugat_.bdd_zero(this.ptr()),nugat_);
    }
    
    /**Function********************************************************************

      Synopsis    [Builds the BDD of a cube from a positional array.]

      Description [Builds a cube from a positional array.  The array must
      have one integer entry for each BDD variable.  If the i-th entry is
      1, the variable of index i appears in true form in the cube; If the
      i-th entry is 0, the variable of index i appears complemented in the
      cube; otherwise the variable does not appear in the cube.  Returns a
      pointer to the BDD for the cube if successful; NULL otherwise.]

      SideEffects [None]

      SeeAlso     [Cudd_bddComputeCube Cudd_IndicesToCube Cudd_BddToCubeArray]

    ******************************************************************************/
    
    
    public Bdd CubeArrayToBdd(int[] array){
        return new Bdd ((nugat_.Cudd_CubeArrayToBdd(this.ptr(), array)),nugat_);
    }
    
    /**
     * Do an and between a and b.
     * @param bdd_ptr_a
     * @param bdd_ptr_b
     * @return bdd_ptr
     */
    public Bdd bddAnd(Bdd a, Bdd  b){
        return new Bdd (nugat_.bdd_and(this.ptr(), a.ptr(), b.ptr()),nugat_);
    }
    
    /**
     * Do an or between a and b
     * @param bdd_ptr_a
     * @param bdd_ptr_b
     * @return bdd_ptr
     */
    public Bdd bddOr( Bdd a, Bdd b){
        return new Bdd (nugat_.bdd_or(this.ptr(), a.ptr(), b.ptr()),nugat_);
    }
    
    /**
     * copy constructor
     * @param dd_node
     * @return bdd_ptr
     */
    public Bdd bddDup(Bdd dd_node){
        return new Bdd(nugat_.bdd_dup(dd_node.ptr()),nugat_);
    }
    
    
    public void bddFree(Bdd dd_node){
        nugat_.bdd_free(this.ptr(),dd_node.ptr());
    }
    
    /**
     * Applies logical AND to the corresponding discriminants
  of f and g and stores the result in f. f and g must be two BDDs. The
  result is referenced.
     * 
     * @param bdd_ptr_a
     * @param bdd_ptr_b
     * @return bdd_ptr
     */
    public Bdd bddAndAccumulate ( Bdd a, Bdd b){
        Bdd result;
        result = bddAnd(a, b);
        bddFree(a);
        a = result;
        return a;
    }
    
    
    /**
     * Applies logical OR to the corresponding discriminants
  of f and g and stores the result in f. f and g must be two BDDs. The
  result is referenced.
     * 
     * @param bdd_ptr_a
     * @param bdd_ptr_b
     * @return bdd_ptr
     */
    public Bdd bddOrAccumulate ( Bdd a, Bdd b){
        Bdd result;
        result = bddOr(a, b);
        bddFree(a);
        a = result;
        return a;
    }
    
    public Bdd bddNot(Bdd fn){
        return new Bdd(nugat_.bdd_not(this.ptr(), fn.ptr()),nugat_);
    }
    
    
    public boolean bddIsZero(Bdd bdd){
        if (nugat_.bdd_is_zero(this.ptr(), bdd.ptr())==1)
            return true;
        else if (nugat_.bdd_is_zero(this.ptr(), bdd.ptr())==0)
            return false;
        else
            throw new RuntimeException("DdManager :: uncorrect return value in C code");
    }
    
    public boolean bddIsOne(Bdd bdd){
        if (nugat_.bdd_is_one(this.ptr(), bdd.ptr())==1)
            return true;
        else if (nugat_.bdd_is_one(this.ptr(), bdd.ptr())==0)
            return false;
        else
            throw new RuntimeException("DdManager :: uncorrect return value in C code");
    }
    
    public boolean bddIsnotZero(Bdd f){
        if (nugat_.bdd_isnot_zero(this.ptr(), f.ptr()) == 1)
            return true;
        else if (nugat_.bdd_isnot_zero(this.ptr(), f.ptr())==0)
            return false;
        else
            throw new RuntimeException("DdManager :: uncorrect return value in C code");
    }
    
    public int bddSize(Bdd fn){
        return (nugat_.bdd_size(this.ptr(), fn.ptr()));
    }

    /**Function********************************************************************

      Synopsis           [Returns the BDD variable with index <code>index</code>.]

      Description        [Retrieves the BDD variable with index <code>index</code>
      if it already exists, or creates a new BDD variable. Returns a
      pointer to the variable if successful; a failure is generated
      otherwise. The returned value is referenced.]

      SideEffects        []

      SeeAlso            [bdd_new_var_at_level add_new_var_at_level]

    ******************************************************************************/
    
    public Bdd bddNewVarWithIndex(int index){
        return new Bdd(nugat_.bdd_new_var_with_index(this.ptr(), index),nugat_);
    }
    
    
    /**
     * Quantify out all variables not in the mask
     * @param keepVariables
     * @return 
     */
    public Bdd extractSubset(Bdd f,Vector<Bdd> vars, Vector<Bdd> maskVars){
        return new Bdd(nugat_.Cudd_SubsetWithMaskVars(this.ptr(),
                f.ptr(),
                convertVecToPointerArray(vars),
                vars.size(),
                convertVecToPointerArray(maskVars),
                maskVars.size()),nugat_);
    }
    
    public Bdd existAbstract(Bdd f, Bdd var){  
        Bdd ret = new Bdd(nugat_.Cudd_bddExistAbstract(this.ptr(),
                f.ptr(),
                var.ptr()),nugat_);
        bddRef(ret);
        //bddFree(var);
        return ret; 
    }
    
    
    public void bddRef(Bdd bdd){
        nugat_.bdd_ref(bdd.ptr());
    }
    
    public Bdd existAbstract(Bdd f, Vector<Bdd> mask){
        Bdd res = bddDup(f);
        
        for (int i = 0; i < mask.size(); ++i)
            res = existAbstract(res, mask.get(i));
        
        return res;
    }
    
    private Pointer[] convertVecToPointerArray(Vector<Bdd> vec){
        int size = vec.size();
        Pointer[] array = new Pointer[size];
        
        for (int i=0; i < size; ++i){
            array[i] = vec.get(i).ptr();
        }
        
        return array;
    }
}
